Inference at * 1 2 1 
Iof proof for Lemma decidable implies better:

.....unproved Inclusion subgoal..... NILNIL

1. P : 
2. Q : x:P.
3. Dec(P)
4. P
  Q  Type 

latex

 by RenameVar `x' 4 THEN IsectHD x 2 THEN Auto 

latex

 .

Definitions

t  T,